(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 8))
(let ((e3 5))
(let ((e4 1))
(let ((e5 (- v0 v1)))
(let ((e6 (- v1)))
(let ((e7 (- v0 v1)))
(let ((e8 (* v1 e5)))
(let ((e9 (- v1)))
(let ((e10 (* e6 e7)))
(let ((e11 (- e6)))
(let ((e12 (* v0 e9)))
(let ((e13 (- e12)))
(let ((e14 (- e12 v0)))
(let ((e15 (+ e9 e11)))
(let ((e16 (- e10)))
(let ((e17 (- e6 e6)))
(let ((e18 (+ v1 e16)))
(let ((e19 (+ v1 e17)))
(let ((e20 (+ e18 e19)))
(let ((e21 (* e12 v0)))
(let ((e22 (- e7 e15)))
(let ((e23 (- e18)))
(let ((e24 (- e8 e16)))
(let ((e25 (/ e2 e2)))
(let ((e26 (- v1 e24)))
(let ((e27 (* (- e2) v1)))
(let ((e28 (/ e4 (- e2))))
(let ((e29 (+ e15 e9)))
(let ((e30 (* e26 e14)))
(let ((e31 (+ e11 e18)))
(let ((e32 (/ e2 e4)))
(let ((e33 (- e16)))
(let ((e34 (* e26 e4)))
(let ((e35 (+ e16 e27)))
(let ((e36 (/ e3 (- e2))))
(let ((e37 (> e20 e27)))
(let ((e38 (< e28 e33)))
(let ((e39 (> e36 e22)))
(let ((e40 (= e9 e7)))
(let ((e41 (>= v1 e26)))
(let ((e42 (= e33 e35)))
(let ((e43 (>= e16 e36)))
(let ((e44 (>= e17 e17)))
(let ((e45 (>= e14 e18)))
(let ((e46 (>= e19 e29)))
(let ((e47 (= e11 e34)))
(let ((e48 (>= e29 e23)))
(let ((e49 (<= e33 e11)))
(let ((e50 (= e10 e17)))
(let ((e51 (>= e20 e10)))
(let ((e52 (>= e25 e5)))
(let ((e53 (< e34 v0)))
(let ((e54 (= e21 e34)))
(let ((e55 (= e5 e25)))
(let ((e56 (= e31 e31)))
(let ((e57 (>= e7 e20)))
(let ((e58 (<= e15 v0)))
(let ((e59 (<= e17 e31)))
(let ((e60 (distinct e31 e23)))
(let ((e61 (< e12 e18)))
(let ((e62 (< e8 e34)))
(let ((e63 (< e21 e29)))
(let ((e64 (distinct e5 e22)))
(let ((e65 (> e30 e29)))
(let ((e66 (= e8 e18)))
(let ((e67 (<= e30 e32)))
(let ((e68 (> e8 e30)))
(let ((e69 (<= e33 e25)))
(let ((e70 (<= v0 e34)))
(let ((e71 (> v0 e16)))
(let ((e72 (<= e12 e35)))
(let ((e73 (>= e33 e7)))
(let ((e74 (<= e16 e26)))
(let ((e75 (distinct e31 e18)))
(let ((e76 (< e13 e19)))
(let ((e77 (< e9 e12)))
(let ((e78 (<= e24 e12)))
(let ((e79 (distinct e17 v1)))
(let ((e80 (distinct e26 v0)))
(let ((e81 (< e19 e20)))
(let ((e82 (distinct e26 e6)))
(let ((e83 (> v0 v1)))
(let ((e84 (> e14 e26)))
(let ((e85 (< v0 e20)))
(let ((e86 (> e36 e24)))
(let ((e87 (distinct e28 e27)))
(let ((e88 (>= e24 e31)))
(let ((e89 (>= e32 e31)))
(let ((e90 (< e9 e6)))
(let ((e91 (> e16 e19)))
(let ((e92 (>= e6 e19)))
(let ((e93 (<= e30 e16)))
(let ((e94 (= e29 e9)))
(let ((e95 (<= v1 e25)))
(let ((e96 (= e12 e21)))
(let ((e97 (= e33 e13)))
(let ((e98 (> e9 e31)))
(let ((e99 (= e22 e30)))
(let ((e100 (< v1 e17)))
(let ((e101 (>= e8 v1)))
(let ((e102 (>= v1 e33)))
(let ((e103 (> e6 e16)))
(let ((e104 (< e20 e7)))
(let ((e105 (distinct e16 e20)))
(let ((e106 (distinct e11 e24)))
(let ((e107 (> e16 e27)))
(let ((e108 (distinct e32 e19)))
(let ((e109 (> v0 e23)))
(let ((e110 (= e29 e29)))
(let ((e111 (<= e28 e6)))
(let ((e112 (<= e10 e32)))
(let ((e113 (< e8 e9)))
(let ((e114 (< e35 e16)))
(let ((e115 (= e7 e27)))
(let ((e116 (<= v0 e26)))
(let ((e117 (>= e32 v0)))
(let ((e118 (distinct e26 e16)))
(let ((e119 (distinct e13 e9)))
(let ((e120 (> e18 e16)))
(let ((e121 (distinct e5 e23)))
(let ((e122 (>= v0 e18)))
(let ((e123 (>= e8 e30)))
(let ((e124 (<= e20 e27)))
(let ((e125 (<= e15 e28)))
(let ((e126 (distinct e13 e10)))
(let ((e127 (> e5 e6)))
(let ((e128 (< e26 e6)))
(let ((e129 (< v1 e25)))
(let ((e130 (< e17 e15)))
(let ((e131 (<= e13 e10)))
(let ((e132 (distinct e35 e10)))
(let ((e133 (= e32 e18)))
(let ((e134 (< e17 e30)))
(let ((e135 (>= e6 e5)))
(let ((e136 (<= e33 e16)))
(let ((e137 (> e31 e27)))
(let ((e138 (> e15 e22)))
(let ((e139 (> e30 e33)))
(let ((e140 (= v1 e27)))
(let ((e141 (>= e7 e15)))
(let ((e142 (> e21 e14)))
(let ((e143 (distinct e11 e11)))
(let ((e144 (= e26 e6)))
(let ((e145 (> v1 e36)))
(let ((e146 (distinct e27 e17)))
(let ((e147 (> e6 v1)))
(let ((e148 (>= e34 e17)))
(let ((e149 (= e112 e72)))
(let ((e150 (=> e97 e119)))
(let ((e151 (or e82 e64)))
(let ((e152 (or e121 e115)))
(let ((e153 (=> e126 e104)))
(let ((e154 (or e105 e39)))
(let ((e155 (not e88)))
(let ((e156 (xor e149 e103)))
(let ((e157 (= e111 e93)))
(let ((e158 (ite e153 e47 e130)))
(let ((e159 (or e40 e89)))
(let ((e160 (= e154 e70)))
(let ((e161 (or e133 e66)))
(let ((e162 (=> e67 e50)))
(let ((e163 (and e77 e49)))
(let ((e164 (xor e158 e95)))
(let ((e165 (xor e51 e46)))
(let ((e166 (xor e69 e134)))
(let ((e167 (and e78 e129)))
(let ((e168 (=> e150 e58)))
(let ((e169 (= e140 e60)))
(let ((e170 (and e123 e52)))
(let ((e171 (ite e106 e165 e117)))
(let ((e172 (xor e163 e107)))
(let ((e173 (or e167 e141)))
(let ((e174 (not e173)))
(let ((e175 (xor e101 e38)))
(let ((e176 (= e85 e128)))
(let ((e177 (and e131 e125)))
(let ((e178 (and e122 e118)))
(let ((e179 (not e59)))
(let ((e180 (and e91 e79)))
(let ((e181 (ite e43 e98 e73)))
(let ((e182 (and e180 e132)))
(let ((e183 (xor e65 e145)))
(let ((e184 (and e120 e174)))
(let ((e185 (ite e157 e137 e178)))
(let ((e186 (=> e53 e147)))
(let ((e187 (and e183 e144)))
(let ((e188 (=> e127 e109)))
(let ((e189 (ite e161 e184 e86)))
(let ((e190 (xor e136 e48)))
(let ((e191 (= e55 e45)))
(let ((e192 (not e171)))
(let ((e193 (and e152 e146)))
(let ((e194 (and e175 e76)))
(let ((e195 (=> e162 e156)))
(let ((e196 (= e192 e139)))
(let ((e197 (xor e71 e168)))
(let ((e198 (not e135)))
(let ((e199 (xor e179 e68)))
(let ((e200 (or e56 e142)))
(let ((e201 (and e160 e96)))
(let ((e202 (or e164 e110)))
(let ((e203 (or e155 e181)))
(let ((e204 (not e191)))
(let ((e205 (ite e113 e189 e75)))
(let ((e206 (and e102 e81)))
(let ((e207 (and e151 e201)))
(let ((e208 (or e138 e177)))
(let ((e209 (= e188 e62)))
(let ((e210 (not e200)))
(let ((e211 (and e124 e169)))
(let ((e212 (or e197 e108)))
(let ((e213 (and e37 e186)))
(let ((e214 (not e208)))
(let ((e215 (and e100 e44)))
(let ((e216 (not e116)))
(let ((e217 (= e99 e204)))
(let ((e218 (not e148)))
(let ((e219 (= e211 e211)))
(let ((e220 (and e84 e212)))
(let ((e221 (and e74 e206)))
(let ((e222 (not e182)))
(let ((e223 (ite e94 e217 e207)))
(let ((e224 (= e176 e202)))
(let ((e225 (xor e159 e215)))
(let ((e226 (ite e187 e203 e166)))
(let ((e227 (=> e92 e223)))
(let ((e228 (not e209)))
(let ((e229 (=> e199 e90)))
(let ((e230 (xor e227 e205)))
(let ((e231 (or e87 e170)))
(let ((e232 (= e194 e172)))
(let ((e233 (and e221 e216)))
(let ((e234 (xor e218 e54)))
(let ((e235 (=> e63 e198)))
(let ((e236 (ite e80 e57 e231)))
(let ((e237 (ite e114 e233 e220)))
(let ((e238 (= e230 e226)))
(let ((e239 (and e41 e222)))
(let ((e240 (ite e236 e213 e193)))
(let ((e241 (=> e195 e83)))
(let ((e242 (or e42 e240)))
(let ((e243 (=> e61 e232)))
(let ((e244 (not e228)))
(let ((e245 (not e219)))
(let ((e246 (not e239)))
(let ((e247 (ite e229 e234 e190)))
(let ((e248 (= e185 e245)))
(let ((e249 (= e248 e224)))
(let ((e250 (ite e249 e225 e237)))
(let ((e251 (xor e238 e214)))
(let ((e252 (and e246 e246)))
(let ((e253 (= e252 e210)))
(let ((e254 (=> e253 e250)))
(let ((e255 (=> e143 e235)))
(let ((e256 (=> e247 e251)))
(let ((e257 (and e196 e243)))
(let ((e258 (and e242 e242)))
(let ((e259 (= e255 e257)))
(let ((e260 (= e241 e258)))
(let ((e261 (xor e259 e259)))
(let ((e262 (not e244)))
(let ((e263 (= e254 e260)))
(let ((e264 (=> e261 e262)))
(let ((e265 (and e256 e256)))
(let ((e266 (ite e263 e263 e263)))
(let ((e267 (=> e264 e266)))
(let ((e268 (not e267)))
(let ((e269 (not e265)))
(let ((e270 (=> e268 e268)))
(let ((e271 (= e270 e269)))
e271
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
